I.A. Field
The present disclosure is related to image and pre-image computation. Specifically, this disclosure teaches a technique that combines Binary Decision Diagram (BDD)-based techniques and Satisfiability Testing (SAT)-based techniques to exploit their complementary benefits.
I.B. Background
Image and pre-image computation play a central role in symbolic state space traversal, which is at the core of a number of applications in Very Large Scale Integrated Circuits (VLSI) Computer Aided Design (CAD) like verification, synthesis, and testing. Exact reachability analysis for sequential system verification is emphasized in this disclosure, though the techniques can also be used for exact invariant checking, exact model checking, approximate reachability analysis, approximate invariant checking, and approximate model checking. For simplicity and easier understanding, only image computation is considered. It should be noted that, the techniques presented could be used for pre-image computation as well.
I.B.1. BDD-based Methods
Verification techniques based on symbolic state space traversal rely on efficient algorithms based on BDDs for computing the image of an input set over a Boolean relation. For further details on symbolic state space traversal, see J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill; and Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design, 13(4):401-424, April 1994, and O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines using symbolic execution. In Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, Volume 407 of Lecture Notes in Computer Science, pages 365-373, June 1989. For further details on BDDs, see R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677-691, August 1986.
The input set for the verification problem is the set of present states P, and the Boolean relation is the transition relation T, i.e., the set of valid present-state, next-state combinations. In case of hardware, it is also convenient to include the primary inputs in the definition of T. The use of BDDs to represent the characteristic function of the relation, the input, and the image set, allows image computation to be performed efficiently through Boolean operations and variable quantification. As an example of an application, the set of reachable states is computed by starting from a set P which denotes the set of initial states of a system, and using image computation iteratively, until a fixpoint is reached.
A number of researchers have proposed the use of partitioned transitioned relations, where the BDD for the entire transition relation is not built a priori. See J. R. Burch, E. M. Clarke, and D. E. Long. Representing circuits more efficiently in symbolic model checking, In Proceedings of the 28th Design Automation Conference, pages 403-407, June 1991; and H. J. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli. Implicit state enumeration of finite state machines using BDDs. In Proceedings of the International Conference on Computer-Aided Design, pages 130-133, 1990.
Typically, the partitions are represented using multiple BDDs, and their conjunction is interleaved with early variable quantification during image computation. Many heuristics have been proposed to find a good quantification schedule, i.e., an ordering of the conjunctions which minimizes the number of peak variables. For more details, see D. Geist and I. Beer. Efficient model checking by automatic ordering of transition relation partitions, in Proceedings of the International Conference on Computer-Aided Verification, Volume 818 of Lecture Notes in Computer Science, pages 299-310, 1994; and R. K. Ranjan, A. Aziz, R. K. Brayton, B. F. Plessier, and C. Pixley. Efficient BDD algorithms for ESM synthesis and verification, in International Workshop for Logic Synthesis, May 1995. Lake Tahoe, Calif. Further, there has also been an interest in using disjunctive partitions of the transition relations and state sets, which effectively splits the image computation into smaller sub-problems. For more details, see G. Cabodi, P. Camurati, and S. Quer. Improving the efficiency of BDD-based operators by means of partitioning, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems , 18(5):545-556, May 1999; I.-H. Moon, J. Kukula, K. Ravi, and F. Somenzi. To split or to conjoin: The question in image computation, in Proceedings of the Design Automation Conference, pages 23-28, June 2000; and A. Narayan, A. J. Isles, J. Jam, H. K. Brayton, and A. Sangiovanni-Vincentelhi. Reachability analysis using partitioned ROBDDs, in Proceedings of the International Conference on Computer-Aided Design, pages 388-393, 1997.
Importantly, BDD-based techniques work well when it is possible to represent the sets of states and the transition relation using BDDs. The representation-can be as a whole, or in a usefully partitioned form. However, BDD size is very sensitive to various factors including: the number of variables, variable ordering, and the nature of the logic expressions being represented. In spite of a large body of conventional work, the verification techniques based purely on BDD technique have been unreliable for designs of realistic size and functionality.
I.B.2. Combining BDDs with SAT-based Methods
On the other hand, an alternative technique used extensively in testing applications, uses Conjunctive Normal Form (CNF) to represent transition relation and further, uses Boolean Satisfiability Checking (SAT) for performing analysis. For more details, see T. Larrabee., Test pattern generation using Boolean satisfiability, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems , 11(1):4-15, January 1992. SAT solver technology has improved significantly in recent years with a number of sophisticated packages now available, e.g. J. P. Marquez-Silva, Grasp package, http://algos.inesc.pt/{tilde over ( )}jpms/software.html.
For checking equivalence of two given combinational circuits C1 and C2, a typical approach is to prove that the XOR of their corresponding outputs can never evaluate to 1, as shown in FIG. 1. Such an XOR of the corresponding output is also called the miter circuit output. A proof for the above proposition can be provided either by building a BDD for the miter, or by using a SAT solver to prove that no satisfying assignment exists for the miter output. In cases where the two methods fail individually, BDDs and SAT can also be combined, for example, in the manner shown in FIG. 1. A cut is identified in the miter circuit to divide the circuit into, two parts: the part PI of the circuit between the circuit inputs and the cut, and the part PO of the circuit between the cut and the output. A BDD is built for PO, while PI is represented in CNF. A SAT solver then tries to enumerate all valid combinations at the cut using the CNF for PI, while checking that it is not contained in the on-set of the BDD for PO. See A. Gupta and P. Ashar. Integrating a Boolean satisfiability checker and BDDs for combinational verification. In Proceedings of the VLSI Design Conference, January 1998. Enumerating the valid combinations at the cut corresponds exactly to computing the image of the input set over the Boolean relation corresponding to PI. Other ways of combining BDDs and SAT for equivalence checking have also been proposed. See J. Burch and V. Singhal. Tight integration of combinational verification methods. In Proceedings of the International Conference on Computer-Aided Design, pages 570-576, 1998.
For property checking, the effectiveness of SAT solvers for finding bugs has also been demonstrated in the context of bounded model checking and symbolic reachability analysis. See P. A. Abdulla, P. Bjesse, and N. Een. Symbolic reachability analysis based on SAT-solvers. In Tools and Algorithms for the Analysis and Construction of Systems (TACAS), 2000, A. Biere, A. Cimatti, B. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Tools and Algorithms for the Analysis and Construction of Systems (TACAS), Volume 1579 of Lecture Notes in Computer Science, 1999, and P. Williams, A. Biere, E. M. Clarke, and A. Gupta. Combining decision diagrams and SAT procedures for efficient symbolic model checking. In Proceedings of the International Conference on Computer-Aided Verification, Volume 1855 of Lecture Notes in Computer Science, pages 124-138, 2000. The common theme is to convert the problem of interest into a SAT problem, by devising the appropriate propositional Boolean formula, and to utilize other non-canonical representations of state sets. However, they all exploit the known ability of SAT solvers to find a single satisfying solution when it exists. However, no attempt has been made to formulate the problems in a way that a SAT solver is used to find all satisfying solutions.
In this respect, the disclosed technique should be distinguished from Moon et al., who independently formulated a decomposition paradigm. See I.-H. Moon, J. Kukula, K. Ravi, and F. Somenzi. To split or to conjoin: The question in image computation. In Proceedings of the Design Automation Conference, pages 23-28, June 2000. However, there are significant differences in the details that are discussed in section IV.E.
The necessary background on a typical SAT decision procedure is in the next sub-section. The preferred embodiment is discussed in detail in section IV. Towards the end, experimental results for reachability analysis, using an embodiment of the present invention, are provided. The results validate the individual ideas and the overall approach of the disclosed techniques.
I.B.3. Satisfiability Checking (SAT)
The Boolean Satisfiability (SAT) problem is a well-known constraint satisfaction problem with many applications in computer-aided design, such as test generation, logic verification and timing analysis. Given a Boolean formula, the objective is to either find an assignment of 0-1 values to the variables so that the formula evaluates to true, or establish that such an assignment does not exist. The Boolean formula is typically expressed in Conjunctive Normal Form (CNF), also called product-of-sums form. Each sum term (clause) in the CNF is a sum of single literals, where a literal is a variable or its negation. An n-clause is a clause with n literals. For example, (vi+vjxe2x80x2+vk) is a 3-clause. In order for the entire formula to evaluate to 1, each clause must be satisfied, i.e., evaluate to 1.
The complexity of this problem is known to be NP-Complete. In practice, most of the conventional SAT solvers are based on the Davis-Putnam algorithm. See M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the ACM, 7:201-205, 1960. The basic algorithm begins from an empty assignment, and proceeds by assigning a 0 or 1 value to one free variable at a time. After each assignment, the algorithm determines the direct and transitive implications of that assignment on other variables, typically called bounding. If no contradiction is detected during the implication procedure, the algorithm picks the next free variable, and repeats the procedure. Otherwise, the algorithm attempts a new partial assignment by complementing the most recently assigned variable for which only one value has been tried so far. This step is called backtracking. The algorithm terminates either when all clauses have been satisfied and a solution has been found, or when all possible assignments have been exhausted. The algorithm is complete in that it will find a solution if it exists.
Pseudo code for the basic Davis-Putnam search procedure is shown in FIG. 2. The function and variable names have obvious meanings. This procedure has been refined over the years by means of enhancements to the Implications ( ), Bound( ), Backtrack ( ), Next_free_var( ) and Val( ) functions. The GRASP work proposed the use of non-chronological backtracking by performing a conflict analysis, and addition of conflict clauses to the database in order to avoid repeating the same contradiction in the future. See J. P. Marques-Silva and K. A. Sakallah. Grasp: A new search algorithm for satisfiability. In Proceedings of the International Conference on Computer-Aided Design, pages 220-227, November 1996.
To overcome the above-mentioned problems in conventional technologies it is an objective of the present invention to provide improved methods for image and pre-image computation.
It is another objective of the present invention to provide improved methods for pruning the search space.
In the disclosed image computation technique BDDs are used to represent state sets, and a CNF formula to represent the transition relation. All valid next state combinations are enumerated using a backtracking search algorithm for SAT that exhaustively visits the entire space of primary input, present state and next state variables. However, rather than using SAT to enumerate each solution all the way down to a leaf, BDD-based image computation is invoked at intermediate points within the SAT decision procedure, which effectively obtains all solutions below that point in the search tree. The disclosed technique can be regarded as SAT providing a disjunctive decomposition of the image computation into many sub-problems, each of which is handled using BDDs.
To meet the objectives of the present invention, there is provided a method of performing image computation for a system, said method comprising representing the system by a finite state model, representing state sets using Binary Decision Diagrams (BDDs), performing a satisfiabilty checking (SAT) based backtrack search algorithm, wherein, the SAT decomposes the search over an entire solution space into multiple sub-problems, and wherein a BDD-based image computation is used to solve each sub-problem by enumerating multiple solutions from the solution space.
Preferably the method is used to perform, exact or approximatexe2x80x94reachability analysis, invariant checking, or model checking.
Preferably, transition relation of the said finite state model is represented using a conjunctive normal form (CNF).
Preferably, complement of a dynamically changing image set is used as a care-set within the search algorithm.
Preferably, the search in SAT is pruned by using BDD Bounding against an implicit disjunction or conjunction of a given set of BDDs, such that the search continues if a partial assignment to variables satisfies the implicit disjunction or conjunction, and backtracks otherwise, said BDD Bounding is further accomplished by applying said BDD Bounding against the implicit disjunction of BDDs which represent the input set, and applying said BDD Bounding against the implicit conjunction of BDDs which represent care sets for the image set.
Preferably the disjunctive decomposition in SAT is accomplished by assigning values to decision variables chosen according to SAT-based heuristics, such as number of clauses a variable appears in; and BDD-based heuristics, such as size of input set and care-set BDDs cofactored with respect to a variable.
Preferably an extent of disjunctive decomposition in SAT is adaptive.
Still preferably the BDD-based image computation procedure determines the multiple solutions by creating a set of BDDs comprising a BDD for each unsatisfied clauses in the CNF representation, adding an input set BDD to said set of BDDs, projecting partial assignment of variables on BDDs in said set of BDDs, choosing a minimum cost variable to quantify, said choice determined by a cost function depending upon: sizes of BDDs in a subset of said set of BDDs, such that the chosen variable appears in each BDD of said subset, an estimate of the size of the product of BDDs in said subset, sizes of variable support sets of BDDs in said subset, and number of variables that can be quantified; performing conjunction of all BDDs in the subset, along with quantification of the chosen variable, and any other variables to be quantified which do not appear in remaining BDDs in the set of BDDs, the remaining BDDs being said subset removed from said set of BDDs;
replacing the subset of BDDs by result of the conjunction and quantification in the previous step; iterating the steps of choosing a minimum cost variable, performing conjunction with quantification, and replacement until there are no more variables to be quantified, and performing a conjunction of the remaining BDDs in the set with a BDD representing a partial assignment of next-state variables.
Still preferably, a BDD-based sub-problem is initiated based on a cost function depending on a number of unassigned variables, size of Bounding BDDs after projection of assigned variables.
Still preferably, a BDD-based sub-problem can be aborted even after initiation due to resource limitations, whereupon SAT is used to decompose the problem further.
Another aspect of the present invention is to use the above methods for pre-image computation as opposed to image computation.
Yet another aspect of the present invention is a method for pruning a search space in a SAT procedure said method comprising using BDD Bounding against an implicit disjunction or conjunction of a given set of BDDs, continuing search if a partial assignment of variables satisfies the implicit disjunction or conjunction, and backtracking if a partial assignment of variables does not satisfy the implicit disjunction or conjunction.
Preferably BDD Bounding against a single BDD is used multiple times for handling said disjunction, wherein search is continued if and only if a partial assignment of variables satisfies any BDD in the given set; and BDD Bounding against multiple BDDs is used for handling said conjunction.
Still preferably, said BDD Bounding procedure against a single BDD is performed by: setting values of assigned variables in a list; and determining that a partial assignment satisfies the BDD if there exists a path in the BDD to a xe2x80x9conexe2x80x9d node in accordance with said values.
Still preferably, said BDD Bounding procedure against multiple BDDs is performed by setting values of assigned variables in a list, traversing multiple BDDs in a lock-step manner in accordance with said values; and determining that a partial assignment satisfies the conjunction if there exists a path in the lockstep traversal of said BDDs that leads to a xe2x80x9conexe2x80x9d node.